Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    fib(N)  → sel(N,fib1(s(0),s(0)))
2:    fib1(X,Y)  → cons(X,fib1(Y,add(X,Y)))
3:    add(0,X)  → X
4:    add(s(X),Y)  → s(add(X,Y))
5:    sel(0,cons(X,XS))  → X
6:    sel(s(N),cons(X,XS))  → sel(N,XS)
There are 6 dependency pairs:
7:    FIB(N)  → SEL(N,fib1(s(0),s(0)))
8:    FIB(N)  → FIB1(s(0),s(0))
9:    FIB1(X,Y)  → FIB1(Y,add(X,Y))
10:    FIB1(X,Y)  → ADD(X,Y)
11:    ADD(s(X),Y)  → ADD(X,Y)
12:    SEL(s(N),cons(X,XS))  → SEL(N,XS)
The approximated dependency graph contains 3 SCCs: {11}, {9} and {12}.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006